$\forall$$T$:Type, $L$:($T$ List), $n$:\{0..($\parallel$$L$$\parallel$+1)$^{-}$\}, $x$:$T$.
\\[0ex]($x$ $\in$ firstn($n$;$L$)) $\Leftarrow\!\Rightarrow$ ($\exists$$i$:\{0..$n$$^{-}$\}. ($x$ = $L$[$i$]))